goverened gas pool spec #118
Conversation
| spec aptos_framework::governed_gas_pool { | ||
| /// <high-level-req> | ||
| /// No.: 1 | ||
| /// Requirement: The GovernedGasPool resource must exist at the aptos_framework address after initialization. |
| /// Enforcement: Formally verified via [high-level-req-1](initialize). | ||
| /// | ||
| /// No.: 2 | ||
| /// Requirement: Only the aptos_framework address is allowed to initialize the GovernedGasPool. |
| /// Enforcement: Formally verified via [high-level-req-2](initialize). | ||
| /// | ||
| /// No.: 3 | ||
| /// Requirement: Deposits into the GovernedGasPool must be reflected in the pool's balance. |
There was a problem hiding this comment.
I would say you want to prove above that initialization creates a resource account distinct from the aptos_framework address. Then deposits into the GovernedGasPool are reflected in that account's balance.
There was a problem hiding this comment.
When I try to to do ensures with anything resource account related I get the error noted down in the PR description.
| /// Enforcement: Formally verified via [high-level-req-3](deposit), [high-level-req-3.1](deposit_from). | ||
| /// | ||
| /// No.: 4 | ||
| /// Requirement: Only the aptos_framework address can fund accounts from the GovernedGasPool. |
aptos-move/framework/aptos-framework/sources/governed_gas_pool.spec.move
Outdated
Show resolved
Hide resolved
| spec module { | ||
| /// [high-level-req-1] | ||
| /// The GovernedGasPool resource must exist at aptos_framework after initialization. | ||
| invariant exists<GovernedGasPool>(@aptos_framework); |
There was a problem hiding this comment.
The GovernGasPool exists for the aptos_framework cannot be an invariant. You would need an exists implies, i.e., ==>. One thing the GovernedGasPool existing could imply is that the resource account for the GovernedGasPool exists.
There was a problem hiding this comment.
It's passing though, I think because of
spec initialize(aptos_framework: &signer, delegation_pool_creation_seed: vector<u8>) {
requires system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework));
/// [high-level-req-1]
ensures exists<GovernedGasPool>(@aptos_framework);
}
```There was a problem hiding this comment.
I can remove it if you we prefer. I suppose we would need to be doing an init_module for it to be an invariant.
|
@0xmovses do you have any of the |
|
@l-monninger Yes the changes for |
Description
governed_gas_pool.spec.movetransaction_validation.spec.moveType of Change
Which Components or Systems Does This Change Impact?
How Has This Been Tested?
Yes
aptos move prove -f governed_gas_pool && aptos move prove -f transaction_validationKey Areas to Review
IMPORTANT
When the feature
COIN_TO_FUNGIBLE_ASSET_MIGRATIONis enabled, this causes thespec fundingoverned_gas_pool.spec.moveto fail. So, I disabled it and it passes as expected.I would advise us to disable this feature for mainnet as it seems strange to enable as we are not migrating to FA yet. However, if we do want to go to mainnet with this feature enabled, then I would imagine something is wrong with the spec.
NOTE
When trying to call
governed_gas_pool_address()within the governed_gas_pool spec I get the following error@franck44 mentions this is a problem to do with versioning and configuration. I tried it with both
aptos move proveandmovement move prove, but it yields the same result. From the error message it seems that Boogie doesn't have a declaration for create_signer at runtime. So makingensuresfor resource accounts seems tricky.In any case the changes offered here offer some value toward full verification.